#include <malloc.h>
#include <algorithm>
#include <iostream>
#include "../divine/generator/circuit.h"
#include "../divine/symbolics.h"
#define assert_eq(a,b) assert(a == b)
#define assert_neq(a,b) assert(a != b);
#define assert_leq(a,b) assert(a <= b);
#define assert_die() assert(false);
#define BLOB_NO_HASH

// -*- C++ -*- (c) 2010 Petr Rockai <me@mornfall.net>

// Not part of the DiVinE *library* headers.

#ifndef DIVINE_GENERATOR_CUSTOM_API_H
#define DIVINE_GENERATOR_CUSTOM_API_H

#define HINTCOUNT 128

typedef char *CBlob;

typedef struct CPoolGroup
{
    size_t item, used, total;
    char **free; // reuse allocation
    char *current; // tail allocation
    char *last; // bumper
} CPoolGroup;

typedef struct CPool {
    size_t group_count;
    size_t group_struct_size;
    char *group_array;
} CPool;

static inline CPoolGroup *pool_group( CPool *pool, int n ) {
    return (CPoolGroup *)(pool->group_array + n * pool->group_struct_size);
}

#ifdef __cplusplus
namespace divine {
    struct Pool;
};
#endif

#ifdef __cplusplus
extern "C" {
#endif
    CPoolGroup *pool_extend( CPool *pool, int sz );
    void *pool_allocate( CPool *pool, int sz );
  void *pool_allocate_blob( CPool *pool, int sz, uint32_t expl = 0xFFFFFFFF );
#ifdef __cplusplus
}
#endif

/**
 * The C-based interface for cached state generation. Caching in this context
 * means obtaining successor lists from more than one state in a single
 * batch. This is useful since even C-based call into a shared object is
 * relatively costly -- too costly to be done for each state in the state
 * space, if generation of a single state is very cheap otherwise.
 *
 * There are 2 circular buffers involved: one for inputs (the states for which
 * we need successors) and one for outputs (the successors themselves). A third
 * buffer, which has a single number for each of the input states, is used to
 * keep the count of output states corresponding to each of the input states.
 *
 * Additionally, a couple of pointers into the buffer are maintained. 3 point
 * into the input buffer, partitioning it into 3 blocks:
 *
 * - done: <first_done, last_done>
 * - active: (last_done, last_in>
 * - inactive (empty): (last_in, first_done>
 *
 * The output buffer is partitioned into just 2 areas, active and inactive. At
 * the index given by first_out, a first successor of the state at in[last_done
 * + 1] is given (assuming count[last_done + 1] > 0), and so on.
 */
struct SuccessorCache {
    int size; // = HINTCOUNT

    // indices for "in"
    int first_done;
    int last_done; // + 1 = first_in
    int last_in;

    // indices for "out"
    int first_out; // corresponds to first_done
    int last_out; // corresponds to last_done

    int handle; // the handle to continue generation at last_done

    int count[HINTCOUNT * 2];

    CBlob in[HINTCOUNT * 2];
    CBlob out[HINTCOUNT * 4];
};

typedef struct CustomSetup {
#ifdef __cplusplus
    union {
#endif
        CPool *cpool; // the pool to obtain memory for new states from
#ifdef __cplusplus
        divine::Pool *pool;
    };
#endif
    void *custom; // per-instance data; never touched by DiVinE

    int slack; // state data starts at this offset. Set by DiVinE!
    int state_size; // The shared object fills this in. Use 0 for variable.
    int has_property; // set to 1 if this is a Buchi automaton (has accepting
                      // states and we are looking for cycles)
} CustomSetup;

#endif

// -*- C++ -*- (c) 2007, 2008 Petr Rockai <me@mornfall.net

// #include <cstdint> requires C++0x : - (
#include <stdint.h>
#include <iostream>
#include <cstring> // size_t ... d'oh
#include <cassert> // for assert*
#ifndef BLOB_NO_HASH
#include <divine/hash.h>
#endif

#ifndef DIVINE_BLOB_H
#define DIVINE_BLOB_H

namespace divine {

typedef uint32_t hash_t;

struct BlobHeader {
    uint16_t size:14;
    uint16_t permanent:1;
    uint16_t heap:1;
    uint16_t align; // ...
};

/**
 * A pointer to an adorned memory area. Basically an array of bytes which knows
 * its size and allows convenient (albeit type-unsafe) access to contents. The
 * array can be up to 2^14 (16k) bytes, the header is 2 bytes (but occupies 4
 * due to alignment anyway). Copies of the Blob object share the array
 * (i.e. this really behaves as a pointer). Users are expected to manage
 * associated memory explicitly (no reference counting is done, for performance
 * reasons).
 *
 * This structure also provides convenient hashing and comparison. The equality
 * operator (==) is implemented in terms of the array contents, not in terms of
 * pointer equality. The hash provided is due to Jenkins, a design which should
 * be both fast to compute and well-behaved. Both hashing and comparison can be
 * limited to a contiguous range within the whole array.
 */
struct Blob
{
    char *ptr;

    Blob() : ptr( 0 ) {}

    template< typename A >
    Blob( A &a, int size, uint32_t expl = 0xFFFFFFFF ) {
        assert_leq( 1, size );
        ptr = a.allocate( allocationSize( size ) );
        header().size = size;
        header().permanent = 0;
        header().heap = 0;
        header().align = ~expl ? expl : 0; 
        assert_eq( reinterpret_cast< intptr_t >( ptr ) % 4, 0 );
    }

  explicit Blob( int size, uint32_t expl = 0xFFFFFFF ) {
        assert_leq( 1, size );
        ptr = new char[ allocationSize( size ) ];
        header().size = size;
        header().permanent = 0;
        header().heap = 1;
        header().align = ~expl ? expl : 0;
        assert_eq( reinterpret_cast< intptr_t >( ptr ) % 4, 0 );
    }

    explicit Blob( BlobHeader *s ) : ptr( (char*) s ) {}
    explicit Blob( char *s, bool s_is_data = false )
        : ptr( s_is_data ? s - sizeof( BlobHeader ) : s )
    {
        assert_eq( reinterpret_cast< intptr_t >( ptr ) % 4, 0 );
    }

    template< typename A >
    void free( A &a ) {
        if ( !valid() )
            return;
        assert( !header().heap );
        if ( !header().permanent )
            a.deallocate( ptr, allocationSize( size() ) );
    }

    void free() {
        if ( !valid() )
            return;
        assert( header().heap );
        if ( !header().permanent )
            delete[] ptr;
    }

    bool valid() const
    {
        return ptr;
    }

    BlobHeader &header() {
        return *reinterpret_cast< BlobHeader * >( pointer() );
    }

    const BlobHeader &header() const {
        return *reinterpret_cast< BlobHeader * >( pointer() );
    }

    template< typename T >
    T &get( int off = 0 ) {
        return *reinterpret_cast< T * >( data() + off );
    }

    void copyTo( Blob &where ) const
    {
        assert_eq( where.size(), size() );
        std::copy( data(), data() + size(), where.data() );
    }

    template< typename O >
    O write32( O o ) const
    {
        return std::copy( pointer32(),
                          pointer32() + allocationSize( size() ) / 4, o );
    }

    template< typename Alloc, typename In >
    In read32( Alloc *a, In i )
    {
        const int hdr_cnt = allocationSize( 0 ) / 4;
        BlobHeader hdr;
        std::copy( i, i + hdr_cnt, reinterpret_cast< int32_t *>( &hdr ) );

        ptr = a->allocate( allocationSize( hdr.size ) );
        In end = i + allocationSize( hdr.size ) / 4;
        std::copy( i, end, pointer32() );
        return end;
    }

    void setSize( size_t size )
    {
        assert( size <= 0x3FFF );
        header().size = size;
    }

    void clear( int from = 0, int to = 0, char pattern = 0 ) {
        if ( to == 0 )
            to = size();
        std::fill( data() + from, data() + to, pattern );
    }

    size_t size() const
    {
        return header().size;
    }

    static size_t allocationSize( size_t size )
    {
        size_t bytes = size + sizeof( BlobHeader );
        bytes += 3;
        bytes = ~bytes;
        bytes |= 3;
        bytes = ~bytes;
        return bytes;
    }

    char *data() const
    {
        return pointer() ? pointer() + sizeof( BlobHeader ) : 0;
    }

    char *pointer() const
    {
        return ptr;
    }

    int32_t *pointer32() const
    {
        return reinterpret_cast< int32_t * >( ptr );
    }

    bool operator<( const Blob &b ) const {
      int cmp = header().align ? compare2( b, sizeof( BlobHeader ), header().align ) :
        compare( b, 0, size() );
        return cmp < 0;
    }

    bool operator==( const Blob &b ) const {
      int retVal = header().align ? compare2( b, sizeof( BlobHeader ), header().align ) :
        compare( b, 0, size() );
      return retVal == 0;
    }

  int compare2( const Blob &cb, int b, int e ) const
  {
    assert( b <= e );
    const Blob &ca = *this;
    assert( e <= ca.size() );
    assert( e <= cb.size() );

    while ( b <= e - signed(sizeof(intptr_t)) ) {
      intptr_t x = *reinterpret_cast< intptr_t * >( ca.data() + b ),
        y = *reinterpret_cast< intptr_t * >( cb.data() + b );
      if ( x < y ) {
        return -1;
      }
      if ( y < x ) {
        return 1;
      }
      b += sizeof( intptr_t );
    }

    while ( b < e ) {
      char x = ca.data()[b], y = cb.data()[b];
      if ( x < y ) {
        return -1;
      }
      if ( y < x ) {
        return 1;
      }
      ++b;
    }

    return 0;
  }
  
    int compare( const Blob &cb, int b, int e ) const
    {
        assert( b <= e );
        const Blob &ca = *this;
        if ( !(b < ca.size() && b < cb.size()) ) {
            return ca.size() - cb.size();
        }
        if ( !(e <= ca.size() && e <= cb.size()) ) {
            return ca.size() - cb.size();
        }

        while ( b <= e - signed(sizeof(intptr_t)) ) {
            intptr_t x = *reinterpret_cast< intptr_t * >( ca.data() + b ),
                     y = *reinterpret_cast< intptr_t * >( cb.data() + b );
            if ( x < y ) {
                return -1;
            }
            if ( y < x ) {
                return 1;
            }
            b += sizeof( intptr_t );
        }

        while ( b < e ) {
            char x = ca.data()[b], y = cb.data()[b];
            if ( x < y ) {
                return -1;
            }
            if ( y < x ) {
                return 1;
            }
            ++b;
        }

        return 0;
    }

#ifndef BLOB_NO_HASH
    hash_t hash() const
    {
      return (header().align ? hash( sizeof( BlobHeader ), header().align ) :
              hash( 0, header().align ));
    }

    hash_t hash( int from, int to ) const
    {
        uint32_t len, total;
        const char *ptr;

        if ( !valid() || from == to )
            return 0;

        assert_leq( from, to );

        ptr = data() + from;
        len = to - from;
        total = len;

        return jenkins3( ptr, len, 0 );
    }
#endif

};

template< typename N >
inline N unblob( const N &n ) {
    return n;
}

template< typename N >
inline N unblob( Blob b ) {
    return b.get< N >();
}

template<>
inline Blob unblob( Blob b ) {
    return b;
}

}

#endif

using namespace divine;
extern "C" int get_system_successor( CustomSetup *, SMTSystem &, int, char ** );
extern "C" void get_system_initial( CustomSetup *setup, char **to );
extern "C" char *system_show_node( CustomSetup *setup, char *from, int );
extern "C" bool prop_limit_active( CustomSetup *setup, char *st );
extern "C" void system_setup( CustomSetup *setup );
extern "C" bool prop_p2( divine::SMTRep *smt, bool neg );
extern "C" bool prop_s2( divine::SMTRep *smt, bool neg );

#include <iostream>
#include <stdio.h>
int *buchi_state( CustomSetup *setup, char *st ) {
    return (int *)(st + setup->slack + 4 /* FIXME BlobHeader */ - sizeof(int));
}

extern "C" int is_accepting( CustomSetup *setup, char *st, int ) {
    int buchi_st = *buchi_state( setup, st ) + 1;
    if ( buchi_st == 5 ) return true;
    return false;
}

extern "C" int setup( CustomSetup *setup ) {
    setup->slack += sizeof(int);
    system_setup( setup );
}
extern "C" void get_initial( CustomSetup *setup, char **to ) {
    get_system_initial( setup, to );
    *(int *)((*to) + setup->slack - sizeof(int)) = 0;
}
extern "C" char *show_node( CustomSetup *setup, char *st, int l ) {
    char *sys = system_show_node( setup, st, l );
    char *bonk = (char *)malloc( strlen( sys ) + 32 );
    sprintf( bonk, "[LTL: %d] %s", *buchi_state( setup, st ) + 1, sys );
    return bonk;
}
extern "C" int get_successor( CustomSetup *setup, int next, char *from, char **to ) {
    int buchi_next = next >> 24;
    int system_next = next & 0xffffff;
    int buchi_st = *buchi_state( setup, from ) + 1;
    SMTSystem &sys = *(SMTSystem *)setup->custom;
    char *in = from + setup->slack + 4;
    sys.read( in );
    divine::SMTRep *smt = sys._smt;
    if ( buchi_next == 0 ) {
        std::cout << "bn " << buchi_next << std::endl;
        if ( buchi_st == 1 && prop_p2( smt, false ) )
            system_next = get_system_successor( setup, sys, system_next, to );
        else { system_next = 0; smt->pc.back().clear(); }
        if (system_next) {
            *buchi_state( setup, *to ) = 1;
            return (system_next & 0xffffff) | (buchi_next << 24);
        }
        system_next = 1;
        ++ buchi_next; /* done with this one, try next buchi edge */
    }
    if ( buchi_next == 1 ) {
        std::cout << "bn " << buchi_next << std::endl;
        if ( buchi_st == 1 )
            system_next = get_system_successor( setup, sys, system_next, to );
        else { system_next = 0; smt->pc.back().clear(); }
        if (system_next) {
            *buchi_state( setup, *to ) = 0;
            return (system_next & 0xffffff) | (buchi_next << 24);
        }
        system_next = 1;
        ++ buchi_next; /* done with this one, try next buchi edge */
    }
    if ( buchi_next == 2 ) {
        std::cout << "bn " << buchi_next << std::endl;
        if ( buchi_st == 2 && prop_p2( smt, false ) )
            system_next = get_system_successor( setup, sys, system_next, to );
        else { system_next = 0; smt->pc.back().clear(); }
        if (system_next) {
            *buchi_state( setup, *to ) = 2;
            return (system_next & 0xffffff) | (buchi_next << 24);
        }
        system_next = 1;
        ++ buchi_next; /* done with this one, try next buchi edge */
    }
    if ( buchi_next == 3 ) {
        std::cout << "bn " << buchi_next << std::endl;
        if ( buchi_st == 3 && prop_p2( smt, false ) )
            system_next = get_system_successor( setup, sys, system_next, to );
        else { system_next = 0; smt->pc.back().clear(); }
        if (system_next) {
            *buchi_state( setup, *to ) = 3;
            return (system_next & 0xffffff) | (buchi_next << 24);
        }
        system_next = 1;
        ++ buchi_next; /* done with this one, try next buchi edge */
    }
    if ( buchi_next == 4 ) {
        std::cout << "bn " << buchi_next << std::endl;
        if ( buchi_st == 4 && prop_p2( smt, false ) && prop_s2( smt, true ) )
            system_next = get_system_successor( setup, sys, system_next, to );
        else { system_next = 0; smt->pc.back().clear(); }
        if (system_next) {
            *buchi_state( setup, *to ) = 4;
            return (system_next & 0xffffff) | (buchi_next << 24);
        }
        system_next = 1;
        ++ buchi_next; /* done with this one, try next buchi edge */
    }
    if ( buchi_next == 5 ) {
        std::cout << "bn " << buchi_next << std::endl;
        if ( buchi_st == 5 )
            system_next = get_system_successor( setup, sys, system_next, to );
        else { system_next = 0; smt->pc.back().clear(); }
        if (system_next) {
            *buchi_state( setup, *to ) = 4;
            return (system_next & 0xffffff) | (buchi_next << 24);
        }
        system_next = 1;
        ++ buchi_next; /* done with this one, try next buchi edge */
    }
    return 0;
}
